i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da), snd:msg-spec(ds;da),
upd:update-spec(ds;da).
update-spec-decl(upd;ds)
 msg-spec-loc-decl(snd;i;da)
 "ecl"  dom(ds)
 R-Feasible(ecl-machine at i with state ecl

 R-Feasible(A

 R-Feasible(state variables ds

 R-Feasible(actions da

 R-Feasible(sends snd

 R-Feasible(updates upd)
 (R:Realizer.
 (R-has-loc(R;i)
 ( R-Feasible(R)
 ( (kecl-kinds(A) @ fpf-domain(da).
 ( (isrcv(k)
 ( ( (source(lnk(k)) = i  Id  Valtype(da;k)  R-da(R;destination(lnk(k)))(k)?Top)
 ( ( & (destination(lnk(k)) = i  Id  R-da(R;source(lnk(k)))(k)?Void  da(k)?Void))
 ( ecl-machine at i with state ecl

 ( A

 ( state variables ds

 ( actions da

 ( sends snd

 ( updates upd || R) 

latex

Definitions

t  T, P  Q, x:A. B(x), , msg-spec-loc(snd;i), ecl-machine at i with state $eclAstate variables dsactions dasends sndupdates upd, R-icompat(A;B), R-has-loc(R;i), b, False, x:AB(x), Prop, P & Q, x:AB(x), A, True, {T}, SQType(T), Id, s = t, s ~ t, Atom$n, Void, Type, b, P  Q, Unit, left+right, x. t(x), a:A fp B(a), Knd, ecl(ds;da), msg-spec(ds;da), update-spec(ds;da), update-spec-decl(upd;ds), msg-spec-loc-decl(snd;i;da), "$x", x.A(x), Top, IdDeq, x  dom(f), R-Feasible(R), Realizer, KindDeq, f(x)?z, lnk(k), source(l), R-da(R;i), destination(l), Valtype(da;k), isrcv(k), fpf-domain(f), ecl-kinds(x), as @ bs, xL. P(x), A || B, a = b

Lemmas

l all wf, append wf, ecl-kinds wf, fpf-domain wf, isrcv wf, ma-valtype wf, top wf, ldst wf, subtype rel wf, R-da wf, lsrc wf, lnk wf, fpf-cap wf, Kind-deq wf, es realizer wf, R-Feasible wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, msg-spec-loc-decl wf, update-spec-decl wf, update-spec wf, msg-spec wf, ecl wf, Knd wf, fpf wf, R-compat-disjoint, ecl-machine wf, ecl-machine-loc, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bnot wf, not wf, eq id wf, bool wf, Id wf, Id sq, true wf, false wf, assert wf, R-has-loc wf, ecl-machine-icompat, msg-spec-loc-decl-implies